- Title
- Model-driven engineering to enhance the reliability of software development by verifying system properties and detecting clones
- Creator
- Hogavanaghatta Kumaraswamy, Jnanamurthy
- Relation
- University of Newcastle Research Higher Degree Thesis
- Resource Type
- thesis
- Date
- 2019
- Description
- Research Doctorate - Doctor of Philosophy (PhD)
- Description
- Computer software is used in almost every facet of day-to-day life, such as air conditioners, refrigerators, washing machines, transport systems, medical systems, and banking. This dependency gives rise to advantages, such as reductions in manual work and improvements in the quality of work. It is essential to ensure that the software that is used in the above-mentioned applications is correct, to avoid catastrophic failures. The aim of this research is twofold, as outlined below. Firstly, formal methods are used to ensure that the software specification for a system is accurate before implementation of that system. The use of formal methods in model-driven development requires a complete transformation of model-driven engineering (MDE) models to a formal model, and also a need to state specifications for verification after the transformation. There are several techniques to transform MDE models into formal models, but the model transformation is not enough to verify the system unless the specification is stated at the model level. Otherwise, the model designer has to know a formal specification language to specify the properties for verification. Additionally, existing modelling frameworks consume additional time during manual inputting of formal specifications to formal verification tools. Furthermore, existing methods achieve less in accuracy (percentage of specifications specified against required specifications during verification) and may require additional documentation of specifications due to, a designer may forget to include all required specifications in the verification tools for verification due to the larger application.To solve this problem, we use domain-specific modelling techniques to design a modelling framework that allows the specification of formal properties at the model level. The model and specifications are then extracted and transformed into a formal model and formal specifications for verification. The designed modelling framework also provides semantics to derive test cases. The framework performs well in coverage criteria during model-based development, and reduces the time and cost of verification by enabling automation. Secondly, software program classification plays a vital role in the identification of similar functionality, which can be considered as software clones, for re-usability, code optimisation and to avoid bug traversal. There are many existing methods for identifying software clones; however, these methods focus on structure-based analysis to detect clones at the code level. We consider the clone detection process at two levels: model and code (considering MDE models and IEC 61131-3 programs). Furthermore, we present a novel approach to detecting clones at model level using semantic-based analysis. Our method is based on model checking that involves mathematical analysis. Our process is tested with control-flow-based models and yields good results in the detection of model clones. To identify clones in IEC 61131-3 programs, we use an approach based on four different perspectives: 1) software clone prediction, involving prediction of similarity based on the elements present in the programs; 2) structural analysis, involving detection of syntactic code clones in a programs organisation unit; 3) semantic analysis, involving analysis of output variable dependency and input variable impact usage to detect semantic clones; 4) variable interval analysis, involving analysis of each variable interval that passes through the CFG, to collect intervals and use this to analyse and identify clones. Our approach is a combination of structural, semantic and data-interval-based analysis. As a result, our approach is feasible and yields excellent results during detection of clones at the code level.
- Subject
- formal verification; model-driven engineering; software clones
- Identifier
- http://hdl.handle.net/1959.13/1397849
- Identifier
- uon:34364
- Rights
- Copyright 2019 Jnanamurthy Hogavanaghatta Kumaraswamy
- Language
- eng
- Full Text
- Hits: 439
- Visitors: 754
- Downloads: 262
| Thumbnail | File | Description | Size | Format | |||
|---|---|---|---|---|---|---|---|
| View Details Download | ATTACHMENT01 | Thesis | 2 MB | Adobe Acrobat PDF | View Details Download | ||
| View Details Download | ATTACHMENT02 | Abstract | 184 KB | Adobe Acrobat PDF | View Details Download |